tele9752wikiaorg-20200213-history
Policy Based Security Analysis in Enterprise Networks: A Formal Approach
Topic 8 from Advanced Topics 2012 Introduction Today, with the development of the enterprise networks, their organizations are becoming increasingly dependent on them in terms of the services, operations and management. Generally, these networks can be divided into several sub-networks according to different departments or sections, connected through various interface routers. And the accesses between these zones and the external network are governed by the enterprise-wide policy of the organization. Typically, the enterprise-wide security policies are specified abstractly and may contain some hidden service access paths. There are two main challenges about this policy in terms of security management approaches. 1. To check whether the security policy specification contains any conflicting rules. 2. To verify whether the security implementations conform to the enterprise-wide security policy. Related work At present, the research work of enterprise-wide security policy can be classified into three categories: 1. Firewall analysis algorithms and tools; 2. Security policy specification languages; 3. Network security analysis using formal approaches. In terms of the formal approaches, there are two main tools. The first one is the FIREMAN Toolkit, which is able to detect inconsistencies and redundancies in single firewalls and in networks of firewalls. The second one is the SAT-based approach that can verify firewall configurations with respect to security policy requirements. But the notion of hidden access paths and formalizing the verification problem in their presence has not been addressed earlier. This results in the fact that the distributed ACL implementation may not satisfy the policy due to two reasons. First of all, there may have some unblocked hidden service access paths in the policy specification. As a result, the ACL implementation in the network may violate one or more policy rules implicitly. Secondly, the policy specification may be correct and conflict-free, but the combined effect of the ACL rules may not conform to the policy. Motivating example The motivation behind this present work is to develop a formal verification framework to analyze security implementations in enterprise networks. A typical enterprise network is shown in figure 2, which consists of various network zones and sub-zones. Now, consider the following enterprise-wide security policy for the network: 1. Internet (http) access is NOT allowed from the ZONE_1. 2. Internet (http) access is allowed from ZONE_2. 3. ssh access from ZONE_1 to ZONE_2 is allowed. Consider the following implementation scenario: ACL rule \neg http(ZONE_1, PROXY) is applied to router R4, blocking all incoming http requests from ZONE_1 at R4, satisfying policy 1. However, this does not strictly satisfy the policy because one can ssh/telnet from ZONE_1 to ZONE_2 and then use http to access Internet (which is allowed from ZONE_2) so the http service access is implicity allowed from ZONE_1, even though it is not allowed in the specification. This type of indirect service access paths is named “hidden service access paths”. In order to solve this problem, a correct ACL implementation should be taken into consideration to restrict hidden access paths consistently to satisfy the security policy. In most of the cases, the security policy given to the network administrator is loosely specified and incomplete. The methodology proposed in this paper generates a conflict-free policy model, ( Mp ), from the enterprise-wide security policy, ( Gp ), and then verifies the distributed ACL implementation model, ( Mi ), with the conflict-free policy model. Hence, it is possible to detect the inconsistent service access paths in the implementation. Security Policy Specification Model (SPSM) The security policy of a network defines a set of parameterised functional rules on flow of packets between different zones in the network. The complexity of the security policy depends on a number of factors, such as: 1.Size of the network 2.Number of controlling parameters 3.Dependency amongst the rules. Security Policy Specification Language The SPSL used to specify explicit “permit” and “deny” service access rules across the network zones. The policy specification language can be classified as (a) network topology specification and (b) network services and policy rule specification. Network Topology specification: The following definitions are used to describe the network topology: Zone: Logical unit consisting of workstations, servers in the network. Router: Used for connecting various sub-networks. Interface: Used for connecting link between a zone and a router. The representation of the Zone, Routers and Interfaces are shown in the examples below: Example 1: Zone ZONE_11 10.0.0.0-10.0.255.255; Zone ZONE_12 10.1.0.0-10.1.255.255; Zone ZONE_1 ZONE_12; Example 2: Interface int_R12 172.16.0.13; Interface int_R13 172.16.0.5; Interface int_R14 172.16.0.2; Router R1 int_R13, int_R14; Network services and policy rule specification: The following definitions are used to specify the network services and policy rules: Service: Defined by a network protocol and service port numbers associated with it. Policy rules: Defines service access (permit/deny) path between a source and a destination. Example 3: Network Service service http = TCP = 80; service ssh = TCP AND port<23; Sometimes policy rule also defines service access path between source and destination under some time constraints. Example 4: Static and Temporal Policy Rules deny ssh(ZONE_1, ZONE_2); permit telnet(ZONE_11,ZONE_2, ZONE_12); deny http(ZONE_1, PROXY)= week_day(0800-1700); Hidden Access Path Analysis Hidden access paths may exist in the security policy model between various network service access paths. Hidden access paths may conflict with the existing policy rules. To make the policy model conflict-free, it is required to remove all hidden access paths from the specification. The hidden access paths can be modelled through a set of formulas described in 20 21. Example: Equation 3 and 4 represent static hidden http access paths and equation 5 and 6 represent the temporal (T) hidden http access paths. In this example, to resolve the hidden access paths, the causing rules (left part of equation) are blocked (set as “deny”) by taking negation of each of the formulas. Security Implementation Model The security policies of an enterprise network are implemented, in general, through a set of device specific access control lists (ACL rules) applied to various interface routers in a distributed manner. In an ACL implementation, each ACL file consists of an access control configuration statement and a set of functional rules. The functional rules are logically grouped into an ACL group. The configuration statement holds the binding information of each ACL group to various network interfaces. In the present approach, a model is extracted from the distributed ACL implementation corresponding to a defined security policy specification in an organizational network. This is done in two phases of translation, namely, (a) translating ACL rules into a set of Service Flow Rule Base, (b) generating a conflict-free topology-independent implementation model. Translating ACL rules into Service Flow Rule base Each service flow rule consists of: Rule header: Holds binding information of the rule to an ACL group and the associated network interface. Functional clause: Holds the functional components of each ACL rule. The structure of the service flow rules and the ACL rule translation procedure are summarized in table 1. The ACL translation procedure stores the ACL rules along with the associated ACL group number and router interfaces using the 3-level index structure. First two levels of the index hold the rule binding information and the other level holds the ACL rules (each node on leaf level can hold multiple rules under the same ACL group number). Generating conflict-free topology-independent implementation model The ACL rule base may have various inter-rule conflicts due to rule component dependencies. The paper describes two types of conflicts: rule subsuming conflict and rule over-riding conflict. Rule subsuming conflict example P1 : permit TCP X1, Y1 eq ssh; P2 : deny TCP X, Y eq ssh; The rules P1 and P2 means that ssh service access from any source in X to any destination in Y is ‘denied’ except those where source and destination are X1 and Y1 respectively. To make these rules conflict-free we need two additional new rules P′2 and P’’2 in place of P2. P2\prime : deny TCP (X-X1), Y eq ssh; P2\prime\prime : deny TCP X, (Y-Y1) eq ssh; Rule over-riding conflict example P3 : permit TCP X, Y eq http; P4 : deny TCP X, Y eq http; In the example above, P3 override P4 which means the rules P3 and P4 can’t be hold simultaneously, because the rule order is top down. To make these rules conflict-free deletion of rule P4 from the rule base is required. From the examples above we could resolve rule subsuming and rule overriding conflicts through selective addition/deletion of rules to/from the rule sets associated to a each router interface. After all procedures this rule base represents the final implementation model, M1. SAT-based verification procedure The SAT based approach reduces the verification problem into a Boolean function and checks its satisfiability. In the proposed approach, the policy (Mp) and implementation (Mi) models are functionally reduced into set of Boolean clauses. A SAT query is formulated and it is checked using zChaff SAT solver 13. Boolean reduction of models The extracted policy and ACL implementation models consist of “permit" and “deny" service access rules across various network zones. The Boolean reduction of these models requires mapping the rule components into Boolean variables. The rule components include service(protocol, port number), source zone, destination zone, time-constraints and action. A network zone can be specified as single IP address or range of IP addresses. So, each of the source and destination zones are mapped to 32 Boolean variables. A range of IP addresses can be translated using disjunction (OR) operator. The address ranges with masks can be reduced through a very simple algorithm given in table 2. Similarly, the protocol types and port numbers are mapped into appropriate Boolean variables. In both the models there are time constraints which define their valid periods. Each valid time period may contain day of week, hours and minutes etc. as components. The components of a valid time period can also be mapped into a set of Boolean variables (see table 3). Here, FP, FI, FS, FD and FT are Boolean functions corresponding to the rule components. The parameters in the functions represent the associated Boolean variables. After rule component mapping, the reduction algorithm represents each rule into a Boolean clause (as a conjunction of rule components) and then combines the clauses for different rules into a single Boolean clause based on one action ("permit/1" or "deny/0") (see table 3). Here, the algorithm starts with an initial model X1 assigned to be 1/True. Then, each policy rule is reduced into a Boolean clause. Then, depending on the action component ( gi ), the algorithm incorporates the rule clause in the model using the OR or AND operators for permit and deny actions, respectively. In this way, all the rules are reduced into Boolean clauses and incorporated in the model. SAT solver and SAT query formation The zChaff SAT solver 13 has been used as the verification tool. It is an efficient implementation of the Chaff algorithm for SAT solving. It takes a Boolean formula and checks its satisfiability. The SAT query for the present problem can be stated as: Does the ACL implementation model ( Mi ) exactly matches the policy model ( Mp )?. After translating it to Boolean representation it is provided as input to zChaff SAT solver, which checks the SAT/UNSAT of the formula and provides the output. Implementation and verification results The algorithms presented in this paper are implemented in C programming language under Linux environment. The framework has been tested with various test cases of implementations under defined policy specifications in an enterprise network. Table 4 shows such experimentations for the enterprise network shown in figure 2. It shows SAT/UNSAT of an implementation with respect to the conflict-free policy model, Mp , along with hidden access path removal time, SAT reduction time and zChaff runtime. Here, the SAT result implies that the implementation does not satisfy the policy (i.e. Mp\neq Mi ) whereas the UNSAT result implies implementation satisfies the policy (i.e. Mp = Mi ). The hidden access path removal time indicates the time to generate correct and conflict-free policy model, Mp , from the enterprise-wide policy specification, Gp in SPSL. The SAT reduction time indicates the time required to represent the policy and ACL rule bases into Boolean models and formulating the SAT queries. In each case, a report is generated from the result and SAT instances which may help the network administrator in debugging the policy (ACL) implementation. The report indicates the violating ACL rules which are derived from the SAT instances. For example, in Case2 of the ACL implementation (refer to table 4), telnet access path from ZONE_1 to ZONE_2 has been detected, which in turn violates the policy model, Mp. So, that service access path must be blocked by incorporating an ACL rule: \neg telnet(ZONE_1,ZONE_2) . In this way, the correct ACL implementation can be realized. The framework is also verified with large set of test cases in a typical enterprise network consisting of various network zones and large set of policy rules. The experimental results along with the timing details are shown in table V. Here, P and CP indicates the number of rules in the policy specification ( Gp ) and conflict-free policy model( Mp ) respectively. The I represents the number of ACL rules in the implementation model( Mi ). The V and C indicates the number of Boolean variables and CNF clauses in the SAT query respectively. The Thr, Tsat and Te represent the hidden access path removal time (in seconds), SAT reduction time of the policy and implementation models (in seconds) and zChaff runtime (in milliseconds) respectively. The result (refer to table V) shows the number of policy and ACL rules in Mp and Mi respectively along with the number of Boolean variables and CNF clauses in the SAT query. It also reports the hidden access path removal time from the policy specification along with SAT reduction time and zChaff execution time. The hidden access path removal time is exponentially dependent on the policy rule count as the procedure incorporates linear search on the policy rule base. Here, the rule insertion to (or deletion from) the rule base takes constant amount of time. However, the SAT reduction procedure formulates Boolean expressions for each policy and ACL rule to generate Mp and Mi respectively and then computes CNF expression for f = Mp \oplus Mi . Thus, the SAT reduction time is linearly dependent on the sum of policy and ACL rule count. Typically, for large enterprise network, the number of policy and ACL rules lies within few hundreds. So, the proposed framework will scale considerably well for any standard enterprise networks, namely industrial, commercial, academic etc. Conclusion There is an increasing requirement of validating the distributed security implementations with the organizational security policy in enterprise networks. This problem becomes more complex due to presence of inconsistent hidden service access paths in the network as well as complex security policy constraints. This paper presents a formal verification framework to analyze the security implementations in an enterprise network with respect to a conflict-free security policy model. The major contributions of the work can be stated as follows: - High level modeling of Enterprise-wide security policy ( Gp ) using a policy specification language, SPSL. - Formalizing the hidden access rules and resolving such conflicts from ( Gp ) to generate a conflict-free policy model ( Mp ). The framework uses a O(N^2) algorithm for hidden access path analysis. - Formal modeling of the network topology and distributed ACL implementations which is represented as ( Mi ). - Boolean reduction of the policy and implementation models, ( Mp ) and ( Mi ); verifying their exact matching using a SAT solver. The efficacy of the framework has been demonstrated through case study and experimentations. The proposed methodology has been shown to be correct and scalable. The framework may facilitate the network administrators in designing conflict-free security policies and debugging its ACL implementation in the network. In future, this work can be extended to develop an integrated network security analysis tool for systematic analysis of security implementations with various service access queries. The framework can be also extended with appropriate access control models for making it usable in wireless network security management. Opinions After a thorough analysis of the ideas presented in the paper we have the opinion that the authors conducted a good research of previous related work before undertaking their own. Also, we found the paper to be explained in a clear and understandable way, making it approachable and interesting even for people outside of the research community. On the other hand, regarding the results presented we believe that the exponential complexity of the implemented algorithm makes it hard to replicate in larger enterprise environments. It also seems that the amount of rules tested could be considered insufficient in order to state that the results are scalable to any corporate network. In relation to the presentation of the paper, we think there are a few grammar issues scattered throughout the paper, which is something that should have been corrected prior to submission for peer review. Finally, we believe the future work section should have been more explicit instead of just providing two very broad topics. Paper references 1 Y. Bartal, A. Mayer, K. Nissim, and A. Wool, “Firmato: a novel firewall management toolkit," ACM Trans. Comput. Syst., vol. 22, no. 4, pp. 381- 420, Nov. 2004. 2 E. S. Al-Shaer and H. H. Hamed, “Discovery of policy anomalies in distributed firewalls," in Proc. IEEE INFOCOM’04, pp. 2605-2626, Hong Kong, China, Mar. 2004. 3 T. E. Uribe and S. Cheung, “Automatic analysis of firewall and network intrusion detection system configurations," in Proc. ACM Workshop Formal Methods Security Eng., pp. 66-71, Washington, DC, USA, Oct. 2004. 4 E. S. Al-shaer and H. H. Hamed, “Firewall policy advisor for anomaly discovery and rule editing," in Proc. IFIP/IEEE 8th International Symp. Integrated Netw. Management, pp. 17-30, Colorado Springs, USA, Mar. 2003. 5 L. Yuan, J. Mai, Z. Su, H. Chen, C. Chuah, and P. Mohapatra, “FIREMAN: a toolkit for firewall modeling and analysis," in 27th IEEE Symp. Security Privacy, Oakland, CA, USA, May 2006. 6 A. X. Liu and M. G. Gouda, “Complete redundancy detection in firewalls," in Proc. 19th Annual IFIP Conf. Data Applications Security, pp. 196-209, Aug. 2005. 7 “High level firewall language." Online. Available: http://www.hlfl.org/. Accessed on Apr. 2009. 8 B. Zhang, E. S. Al-Shaer, R. Jagadeesan, J. Riely, and C. Pitcher, “Specifications of a high-level conflict-free firewall policy language for multi-domain networks," in Proc. 12th ACM Symp. Access Control Models Technologies (SACMAT 2007), pp. 185-194, France, June 2007. 9 “CISCO: Configuring IP access lists," CISCO White Papers 23602 edition, July 2007. 10 “Configuring ACL in Huawei switches," Huawei 3 Com Switch 4500G Release Notes, pp. 1-28, Feb. 2009. 11 “Alcatel-OS-LS-6200 User Guide," Part No. 060202-10, pp. 1-762, June 2007. 12 J. D. Guttman and A. L. Herzog, “Rigorous automated network security management," International J. Inf. Security, vol. 4, no. 2, pp. 29-48, 2005. 13 Y. S. Mahajan, Z. Fu, and S. Malik, “Zchaff 2004: an efficient SAT solver," in Proc. 8th International Conf. Theory Application Satisfiability Testing, pp. 360-375, Scotland, June 2005. 14 C. C. Zhang, M. Winslet, and C. A. Gunter, “On the safety and efficiency of firewall policy deployment," in 28th IEEE Symp. Security Privacy, pp. 33-50, Oakland, CA, USA, May 2007. 15 P. Matousek, J. Rab, O. Rysavy, and M. Sveda, “A formal model for network-wide security analysis," in Proc. 15th IEEE International Conf. Workshop ECBS, Belfast, Ireland, 2008. 16 T. Hofmeister, U. Schoning, R. Schuler, and O. Watanabe, “A probabilistic 3-SAT algorithm further improved," in Proc. 19th Annual Symp. Theoretical Aspects Computer Science (SATACS), pp. 192-202, 2002. 17 O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier, SAT Versus UNSAT, Second DIMACS Challenge, D. S. Johnson and M. A. Trick, editors, 1993. 18 L. Zhang and S. Malik, “Towards symmetric treatment of conflicts and satisfaction in quantified Boolean satisfiability," in Proc. 8th International Conf. Principles Practice Constraint Programming (CP 2002), pp. 200-215, 2002. 19 S. Matsumoto and A. Bouhoula, “Automatic verification of firewall configuration with respect to security policy requirements," in Proc. International Workshop Computational Intelligence Security Inf. Syst. (CISIS’08), pp. 123-130, Barcelona, Spain, Oct. 2008. 20 D. Gabby, Ch. Hogger, and J. Robinson, editors, “Temporal Logic," Handbook of Logic in AI and Logic Programming, vol. 4. Oxford University Press, 1995. 21 Y. Venema, “A modal logic for quantification and substitution," L. Csirmaz, D. Gabby and M. de Rijke, editors, Logic Colloquium 92, Veszprem, Hungary, Studies in Logic, Languages and Information. CSLI Publications, Stanford, pp. 293-309, 1995. 22 P. Bera, P. Dasgupta, and S. K. Ghosh, “A verification framework for analyzing security implementations in an enterprise LAN," in Proc. IEEE International Advance Computing Conf. (IACC 09), pp 1008-1015, Mar. 2009. 23 S. K. Ghosh, “Analyzing security policy implementations in enterprise networks–a formal approach," in Indo-US Conf. Workshop Cyber Security, Cyber Crime Cyber Forensic (ICSCF 2009), invited position paper, Kochi, India, July 2009. 24 P. Bera, P. Dasgupta, and S. K. Ghosh, “Formal analysis of security policy implementations in enterprise networks," International J. Computer Netw. Commun., vol. 2009, no. 2, pp 56-73, June 2009. 25 P. Bera, S. K. Ghosh, and P. Dasgupta, “Formal verification of security policy implementations in enterprise networks," in Proc. 5th International Conf. Inf. Syst. Security (ICISS 09), pp. 117-131, Kolkata, India, Dec. 2009.